A:Type, f:(A), L:A List.
aL.
(baL.f(b))
 (L1, L2:A List.
 (L = (L1 @ L2)  A List & (a  L2) & (bL2. f(b)) & (null(L1)  f(last(L1)))) 

latex

Definitions

P  Q, x:A. B(x), last(L), t  T, b, A, null(as), Prop, (x  l), P & Q, as @ bs, x:A. B(x), split_tail(L | x.f(x)), False, x. t(x), , x before y  l, xL. P(x), (xaL.P(x)), x(s), 2of(t), 1of(t), P  Q, P  Q, {a:T}, S  T, l1  l2, {T}, True, b, Unit, T, hd(l), i<j, ij, l[i], if b t else f fi

Lemmas

squash wf, last cons, false wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, bnot wf, true wf, l all fwd, split tail correct, iseg member, split tail max, uni sat imp in uni set, iff imp equal bool, minus mono wrt eq, singleton properties, div unique, eq cons imp eq tls, add cancel in eq, bool decision, assert of eq int, eq int eq true elim, split tail rel, l before wf, bool wf, pi1 wf, split tail wf, pi2 wf, append wf, l member wf, null wf, not wf, assert wf, last wf